Nuprl Lemma : es-pred!-wellfounded 11,40

es:event_system{i:l}. SWellFounded(es-pred!(esee')) 
latex


Definitionsx:AB(x), SWellFounded(R(x;y)), x:AB(x), t  T, event_system{i:l}, es-pred!(esee'), es-E(es), es-pred?(es), es_info(es), EOrderAxioms(E;pred?;info), P  Q, A c B, x:A  B(x)
Lemmasevent system wf

origin